Nuprl Lemma : member-le-max 11,40

L:( List), x:. (x  L (x  imax-list(L)) 
latex


Definitionsx:AB(x), P  Q, t  T, (xL.P(x)), A  B, x:AB(x), P & Q, A, False, , P  Q, P  Q, (x  l), A c B
Lemmasimax-list-ub, l member wf, length wf1, le wf

origin